$\forall$$T$:Type, $l_{1}$, $l_{2}$:($T$ List).
\\[0ex]$l_{1}$ $\leq$ $l_{2}$ $\Leftarrow\!\Rightarrow$ (($\parallel$$l_{1}$$\parallel$ $\leq$ $\parallel$$l_{2}$$\parallel$) c$\wedge$ ($\forall$$i$:$\mathbb{N}$. ($i$ $<$ $\parallel$$l_{1}$$\parallel$) $\Rightarrow$ ($l_{1}$[$i$] = $l_{2}$[$i$] $\in$ $T$)))